Nuprl Lemma : fun_exp_wf
11,40
postcript
pdf
T
:Type,
n
:
,
f
:(
T
T
).
f
^
n
T
T
latex
Definitions
f
^
n
,
t
T
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
,
int
seg
wf
,
compose
wf
,
primrec
wf
origin
T:Type, n:
, f:(T
T). f^n 
TT T:Type, n:, f:(TT). f^n TT Tx:A. B(x)